Erased-cubical-Import.agda:12,5-8
Identifier ∣_∣ is declared erased, so it cannot be used here
when checking that the expression ∣_∣ has type A → ∥ A ∥
